es:ES, p:(E(E + Top)).
(causal-predecessor(es;p) & p-inject(E;E;p))
 (e, e':E. same-thread(es;p;e;e')  (((e < e')  (e = e'))  (e' < e))) 

latex

Definitions	x:A. B(x), P  Q, P & Q, t  T, , P  Q, {T}
Lemmas	same-thread wf, es-E wf, causal-predecessor wf, p-inject wf, top wf, event system wf, thread-p-ordered, es-causl wf, es-causl weakening p-locl